partial ordering

A {relation} R is a partial ordering if it is a {pre-order}

(i.e. it is {reflexive} (x R x) and {transitive} (x R y R z ◦>

x R z)) and it is also {antisymmetric} (x R y R x ◦> x ◦ y).

The ordering is partial, rather than total, because there may

exist elements x and y for which neither x R y nor y R x.

In {domain theory}, if D is a set of values including the

undefined value ({bottom}) then we can define a partial

ordering relation <◦ on D by

x <◦ y if x ◦ bottom or x ◦ y.

The constructed set D x D contains the very undefined element,

(bottom, bottom) and the not so undefined elements, (x,

bottom) and (bottom, x). The partial ordering on D x D is

then

(x1,y1) <◦ (x2,y2) if x1 <◦ x2 and y1 <◦ y2.

The partial ordering on D -> D is defined by

f <◦ g if f(x) <◦ g(x) for all x in D.

(No f x is more defined than g x.)

A {lattice} is a partial ordering where all finite subsets

have a {least upper bound} and a {greatest lower bound}.

("<◦" is written in {LaTeX} as {\sqsubseteq}).

(1995-02-03)